(set-logic QF_LRA)
(set-info :source |
TLP-GP automated DTP to SMT-LIB encoding for planning
by F.Maris and P.Regnier, IRIT - Universite Paul Sabatier, Toulouse

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun St_spy_variable () Real)
(declare-fun t_Init_0 () Real)
(declare-fun t_Goal_6 () Real)
(declare-fun t_BAKE_CERAMIC2_p2_k2_2 () Real)
(declare-fun t_TREAT_CERAMIC2_p2_3 () Real)
(declare-fun t_BAKE_CERAMIC2_p2_k2_3 () Real)
(declare-fun t_BAKE_CERAMIC1_p1_k2_2 () Real)
(declare-fun t_TREAT_CERAMIC1_p1_3 () Real)
(declare-fun t_FIRE_KILN2_k2_2 () Real)
(declare-fun t_BAKE_CERAMIC1_p1_k2_3 () Real)
(declare-fun t_MAKE_STRUCTURE_p1_p2_4 () Real)
(declare-fun t_BAKE_STRUCTURE_p1_p2_k1_5 () Real)
(declare-fun t_BAKE_CERAMIC3_p4_k2_2 () Real)
(declare-fun t_TREAT_CERAMIC3_p4_3 () Real)
(declare-fun t_BAKE_CERAMIC3_p4_k1_3 () Real)
(declare-fun t_FIRE_KILN2_k2_1 () Real)
(declare-fun t_BAKE_CERAMIC3_p3_k2_2 () Real)
(declare-fun t_TREAT_CERAMIC3_p3_3 () Real)
(declare-fun t_FIRE_KILN1_k1_2 () Real)
(declare-fun t_BAKE_CERAMIC3_p3_k1_3 () Real)
(declare-fun t_MAKE_STRUCTURE_p3_p4_4 () Real)
(declare-fun t_FIRE_KILN1_k1_1 () Real)
(declare-fun t_BAKE_STRUCTURE_p3_p4_k1_5 () Real)
(assert (let ((?v_11 (- t_Goal_6 t_BAKE_STRUCTURE_p1_p2_k1_5)) (?v_21 (- t_Goal_6 t_BAKE_STRUCTURE_p3_p4_k1_5)) (?v_15 (- t_BAKE_CERAMIC3_p3_k2_2 t_FIRE_KILN2_k2_1))) (let ((?v_2 (<= ?v_15 15)) (?v_12 (- t_BAKE_CERAMIC3_p4_k2_2 t_FIRE_KILN2_k2_1))) (let ((?v_3 (<= ?v_12 15)) (?v_7 (- t_BAKE_CERAMIC1_p1_k2_2 t_FIRE_KILN2_k2_1))) (let ((?v_4 (<= ?v_7 5)) (?v_6 (- t_BAKE_CERAMIC2_p2_k2_3 t_FIRE_KILN2_k2_1))) (let ((?v_5 (<= ?v_6 10)) (?v_0 (- t_BAKE_CERAMIC2_p2_k2_2 t_FIRE_KILN2_k2_1)) (?v_1 (- t_TREAT_CERAMIC2_p2_3 t_BAKE_CERAMIC2_p2_k2_2)) (?v_8 (- t_TREAT_CERAMIC1_p1_3 t_BAKE_CERAMIC1_p1_k2_2)) (?v_9 (- t_BAKE_CERAMIC1_p1_k2_3 t_FIRE_KILN2_k2_2)) (?v_20 (- t_BAKE_STRUCTURE_p3_p4_k1_5 t_FIRE_KILN1_k1_1))) (let ((?v_19 (<= ?v_20 5)) (?v_10 (- t_BAKE_STRUCTURE_p1_p2_k1_5 t_FIRE_KILN1_k1_1)) (?v_13 (- t_TREAT_CERAMIC3_p4_3 t_BAKE_CERAMIC3_p4_k2_2)) (?v_18 (- t_BAKE_CERAMIC3_p3_k1_3 t_FIRE_KILN1_k1_2))) (let ((?v_17 (<= ?v_18 3)) (?v_14 (- t_BAKE_CERAMIC3_p4_k1_3 t_FIRE_KILN1_k1_2)) (?v_16 (- t_TREAT_CERAMIC3_p3_3 t_BAKE_CERAMIC3_p3_k2_2)) (?v_29 (- t_BAKE_CERAMIC1_p1_k2_3 t_FIRE_KILN2_k2_1)) (?v_28 (> (- t_FIRE_KILN2_k2_2 t_FIRE_KILN2_k2_1) 20))) (let ((?v_24 (or (<= ?v_29 5) ?v_28)) (?v_25 (> (- t_FIRE_KILN2_k2_1 t_FIRE_KILN2_k2_2) 20)) (?v_23 (- t_BAKE_CERAMIC2_p2_k2_2 t_BAKE_CERAMIC2_p2_k2_3)) (?v_22 (- t_BAKE_CERAMIC2_p2_k2_3 t_BAKE_CERAMIC2_p2_k2_2)) (?v_27 (- t_BAKE_CERAMIC1_p1_k2_2 t_BAKE_CERAMIC1_p1_k2_3)) (?v_26 (- t_BAKE_CERAMIC1_p1_k2_3 t_BAKE_CERAMIC1_p1_k2_2)) (?v_38 (- t_BAKE_CERAMIC3_p3_k1_3 t_FIRE_KILN1_k1_1)) (?v_30 (> (- t_FIRE_KILN1_k1_2 t_FIRE_KILN1_k1_1) 8)) (?v_34 (- t_BAKE_CERAMIC3_p4_k1_3 t_FIRE_KILN1_k1_1)) (?v_33 (> (- t_FIRE_KILN1_k1_1 t_FIRE_KILN1_k1_2) 8)) (?v_32 (- t_BAKE_CERAMIC3_p4_k2_2 t_BAKE_CERAMIC3_p4_k1_3)) (?v_31 (- t_BAKE_CERAMIC3_p4_k1_3 t_BAKE_CERAMIC3_p4_k2_2))) (let ((?v_37 (or (<= (- t_BAKE_STRUCTURE_p3_p4_k1_5 t_FIRE_KILN1_k1_2) 5) ?v_33)) (?v_36 (- t_BAKE_CERAMIC3_p3_k2_2 t_BAKE_CERAMIC3_p3_k1_3)) (?v_35 (- t_BAKE_CERAMIC3_p3_k1_3 t_BAKE_CERAMIC3_p3_k2_2))) (and (= St_spy_variable (+ 1 t_Init_0)) (>= t_Goal_6 t_Init_0) (>= (- t_BAKE_CERAMIC2_p2_k2_2 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC2_p2_k2_2) 10) (>= (- t_TREAT_CERAMIC2_p2_3 t_Init_0) 0) (>= (- t_Goal_6 t_TREAT_CERAMIC2_p2_3) 2) (>= (- t_BAKE_CERAMIC2_p2_k2_3 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC2_p2_k2_3) 10) (>= (- t_BAKE_CERAMIC1_p1_k2_2 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC1_p1_k2_2) 15) (>= (- t_TREAT_CERAMIC1_p1_3 t_Init_0) 0) (>= (- t_Goal_6 t_TREAT_CERAMIC1_p1_3) 3) (>= (- t_FIRE_KILN2_k2_2 t_Init_0) 0) (>= (- t_Goal_6 t_FIRE_KILN2_k2_2) 20) (>= (- t_BAKE_CERAMIC1_p1_k2_3 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC1_p1_k2_3) 15) (>= (- t_MAKE_STRUCTURE_p1_p2_4 t_Init_0) 0) (>= (- t_Goal_6 t_MAKE_STRUCTURE_p1_p2_4) 1) (>= (- t_BAKE_STRUCTURE_p1_p2_k1_5 t_Init_0) 0) (>= ?v_11 3) (>= (- t_BAKE_CERAMIC3_p4_k2_2 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC3_p4_k2_2) 5) (>= (- t_TREAT_CERAMIC3_p4_3 t_Init_0) 0) (>= (- t_Goal_6 t_TREAT_CERAMIC3_p4_3) 1) (>= (- t_BAKE_CERAMIC3_p4_k1_3 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC3_p4_k1_3) 5) (>= (- t_FIRE_KILN2_k2_1 t_Init_0) 0) (>= (- t_Goal_6 t_FIRE_KILN2_k2_1) 20) (>= (- t_BAKE_CERAMIC3_p3_k2_2 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC3_p3_k2_2) 5) (>= (- t_TREAT_CERAMIC3_p3_3 t_Init_0) 0) (>= (- t_Goal_6 t_TREAT_CERAMIC3_p3_3) 1) (>= (- t_FIRE_KILN1_k1_2 t_Init_0) 0) (>= (- t_Goal_6 t_FIRE_KILN1_k1_2) 8) (>= (- t_BAKE_CERAMIC3_p3_k1_3 t_Init_0) 0) (>= (- t_Goal_6 t_BAKE_CERAMIC3_p3_k1_3) 5) (>= (- t_MAKE_STRUCTURE_p3_p4_4 t_Init_0) 0) (>= (- t_Goal_6 t_MAKE_STRUCTURE_p3_p4_4) 1) (>= (- t_FIRE_KILN1_k1_1 t_Init_0) 0) (>= (- t_Goal_6 t_FIRE_KILN1_k1_1) 8) (>= (- t_BAKE_STRUCTURE_p3_p4_k1_5 t_Init_0) 0) (>= ?v_21 3) ?v_2 ?v_3 ?v_4 ?v_5 (<= ?v_0 10) (< ?v_0 10) (>= ?v_0 2) (<= ?v_1 8) (>= ?v_1 0) (>= (- t_MAKE_STRUCTURE_p1_p2_4 t_TREAT_CERAMIC2_p2_3) 2) ?v_2 ?v_3 ?v_4 ?v_5 (< ?v_6 10) (>= ?v_6 2) (>= (- t_MAKE_STRUCTURE_p1_p2_4 t_BAKE_CERAMIC2_p2_k2_3) 10) ?v_2 ?v_3 ?v_4 (< ?v_7 5) (>= ?v_7 2) (<= ?v_8 12) (>= ?v_8 0) (>= (- t_MAKE_STRUCTURE_p1_p2_4 t_TREAT_CERAMIC1_p1_3) 3) (<= ?v_9 5) (>= ?v_9 2) (>= (- t_MAKE_STRUCTURE_p1_p2_4 t_BAKE_CERAMIC1_p1_k2_3) 15) (>= (- t_BAKE_STRUCTURE_p1_p2_k1_5 t_MAKE_STRUCTURE_p1_p2_4) 1) ?v_19 (<= ?v_10 5) (< ?v_10 5) (>= ?v_10 1) (>= ?v_11 4) ?v_2 ?v_3 (< ?v_12 15) (>= ?v_12 2) (<= ?v_13 4) (>= ?v_13 0) (>= (- t_MAKE_STRUCTURE_p3_p4_4 t_TREAT_CERAMIC3_p4_3) 1) ?v_17 (<= ?v_14 3) (< ?v_14 3) (>= ?v_14 1) (>= (- t_MAKE_STRUCTURE_p3_p4_4 t_BAKE_CERAMIC3_p4_k1_3) 5) ?v_2 (>= ?v_15 2) (<= ?v_16 4) (>= ?v_16 0) (>= (- t_MAKE_STRUCTURE_p3_p4_4 t_TREAT_CERAMIC3_p3_3) 1) ?v_17 (>= ?v_18 1) (>= (- t_MAKE_STRUCTURE_p3_p4_4 t_BAKE_CERAMIC3_p3_k1_3) 5) (>= (- t_BAKE_STRUCTURE_p3_p4_k1_5 t_MAKE_STRUCTURE_p3_p4_4) 1) ?v_19 (>= ?v_20 1) (>= ?v_21 4) ?v_24 (or ?v_25 (< (- t_BAKE_CERAMIC2_p2_k2_2 t_FIRE_KILN2_k2_2) 10)) (or (>= (- t_BAKE_CERAMIC2_p2_k2_2 t_MAKE_STRUCTURE_p1_p2_4) 1) (< ?v_23 7)) (or (<= ?v_22 0) (> ?v_22 10)) (or (>= ?v_23 3) (> ?v_22 7)) (or (> ?v_23 10) (< (- t_TREAT_CERAMIC2_p2_3 t_BAKE_CERAMIC2_p2_k2_3) 8)) ?v_24 (or ?v_25 (< (- t_BAKE_CERAMIC2_p2_k2_3 t_FIRE_KILN2_k2_2) 10)) ?v_24 (or ?v_25 (< (- t_BAKE_CERAMIC1_p1_k2_2 t_FIRE_KILN2_k2_2) 5)) (or (>= (- t_BAKE_CERAMIC1_p1_k2_2 t_MAKE_STRUCTURE_p1_p2_4) 1) (< ?v_27 10)) (or (<= ?v_26 0) (> ?v_26 15)) (or (>= ?v_27 5) (> ?v_26 10)) (or (> ?v_27 15) (< (- t_TREAT_CERAMIC1_p1_3 t_BAKE_CERAMIC1_p1_k2_3) 12)) (or (<= (- t_BAKE_CERAMIC3_p3_k2_2 t_FIRE_KILN2_k2_2) 15) ?v_25) (or (<= (- t_BAKE_CERAMIC3_p4_k2_2 t_FIRE_KILN2_k2_2) 15) ?v_25) (or ?v_28 (< ?v_29 5)) (or (<= ?v_38 3) ?v_30) (or (<= ?v_34 3) ?v_30) (or ?v_33 (< (- t_BAKE_STRUCTURE_p1_p2_k1_5 t_FIRE_KILN1_k1_2) 5)) (or (>= (- t_BAKE_CERAMIC3_p4_k2_2 t_MAKE_STRUCTURE_p3_p4_4) 1) (< ?v_32 4)) (or (<= ?v_31 0) (> ?v_31 5)) (or (>= ?v_32 1) (> ?v_31 4)) (or (> ?v_32 5) (< (- t_TREAT_CERAMIC3_p4_3 t_BAKE_CERAMIC3_p4_k1_3) 4)) ?v_37 (or ?v_30 (< ?v_34 3)) (or (>= (- t_BAKE_CERAMIC3_p3_k2_2 t_MAKE_STRUCTURE_p3_p4_4) 1) (< ?v_36 4)) (or (<= ?v_35 0) (> ?v_35 5)) (or (>= ?v_36 1) (> ?v_35 4)) (or (> ?v_36 5) (< (- t_TREAT_CERAMIC3_p3_3 t_BAKE_CERAMIC3_p3_k1_3) 4)) ?v_37 (or ?v_30 (< ?v_38 3)))))))))))))
(check-sat)
(exit)
